#!/bin/bash

##################
# Return values:
# 1: parameters or files error
# 2: SAT Solver error
# 10: CPU and GPU solvers outputs match (passed)
# 20: CPU and GPU solvers outputs do not match (failed)
#
##################

# Temporary files
DATE=`date +"%y_%m_%d_%H_%M_%S"`
TMP_FILE=/tmp/test_cnf_${DATE}_${RANDOM}
TMP_CNF=/tmp/test_cnf_cpu_${DATE}_${RANDOM}

# Input files
FILES_PREFIX=$1
CNF=${FILES_PREFIX}".cnf"

# Executables
CUDAPSAT=../Debug/GPUSATSolver
MINISAT=../../../../minisat/core/minisat

if [[ "$#" != 1 ]] && [[ "$#" != 2 ]]
then
	echo "Wrong number of parameters. Expected 1 or 2." >&2
	exit 1
fi

if ! [[ -e "$CNF" ]]
then
	echo "Could not find the CNF file." >&2
	exit 1
fi

if [[ "$#" == 1 ]]
then
	THREADS=1
else
	THREADS=$2

	if [[ "$THREADS" == "0" ]]
	then
		echo "Invalid threads number, should be a positive integer (if you recall your math classes, zero is not a positive integer)." >&2
		exit 1

	fi

	if ! [[ "$THREADS" =~ [1-9][0-9]* ]]
	then
		echo "Invalid threads number, should be a positive integer." >&2
		exit 1
	fi
fi

VARIABLES=`cat $CNF | grep "p cnf" | cut -d " " -f 3`
CLAUSES=`cat $CNF | grep "p cnf" | cut -d " " -f 4`

#echo $VARIABLES $CLAUSES

for i in $(seq 1 $VARIABLES)
do

	let INDEX=$i-1

	CUDAPSAT_RESULT[$INDEX]="u"

done

$CUDAPSAT $CNF -t $THREADS -s u > $TMP_FILE

SAT=`cat $TMP_FILE | egrep "SAT|UNSAT|UNDEF"`
#SOLUTIONS=`cat $TMP_FILE | grep "0"`
SOLUTIONS=(`cat $TMP_FILE | egrep -x "((-)?[1-9][0-9]* )+0"`)

echo "GPU's solution is:"
echo $SOLUTIONS

if [[ $SAT != "UNDEF" ]] && [[ $SAT != "UNSAT" ]] && [[ $SAT != "SAT" ]]
then

	echo "GPU SAT Solver returned an unknown output." >&2
	exit 2

fi

if [[ $SAT == "UNDEF" ]]
then
	echo "CUDA SAT Solver did not return answer..." >&2
	exit 2
fi

if [[ $SAT == "UNSAT" ]]
then

	$MINISAT $CNF 2>&1 > /dev/null
	RESULT=$?

	if [[ $RESULT != "10" ]] && [[ $RESULT != "20" ]]
	then
		echo "An error has occurred on the CPU SAT Solver"
		exit 2
	fi

	if [[ $RESULT == "10" ]]
	then
		echo "NOT MATCHED"
		echo "GPU returns UNSAT while CPU returns SAT"
		exit 20
	fi

	if [[ $RESULT == "20" ]]
	then
		echo "MATCHED"
                echo "Both CPU and GPU returns UNSAT"
		exit 10
	fi



else

	cp $CNF $TMP_CNF

	INDEX=0
	LIT=${SOLUTIONS[$INDEX]}

	while [ $LIT -ne "0" ]
	do
		echo "$LIT 0" >> $TMP_CNF
		let INDEX++
		LIT=${SOLUTIONS[$INDEX]}
	done

	$MINISAT $TMP_CNF 2>&1 > /dev/null
	RESULT=$?

	if [[ $RESULT != "10" ]] && [[ $RESULT != "20" ]]
	then
		echo "An error has occurred on the CPU SAT Solver"
		exit 2
	fi

	if [[ $RESULT == "20" ]]
	then
		echo "NOT MATCHED"
		echo "GPU's solution does not satisfy CPU SAT Solver"
		exit 20
	fi

	if [[ $RESULT == "10" ]]
	then
		echo "MATCHED"
                echo "Both CPU and GPU returns SAT and solutions match"
		exit 10
	fi

fi

